\begin{tabbing}
w{-}automaton($T$;${\it TA}$;$M$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($b$:Id$\rightarrow$($x$:Id$\rightarrow$$T$($x$))$\rightarrow$(${\it TA}$($b$)+Unit))\+
\\[0ex]$\times$($k$:Knd$\rightarrow$kindcase($k$; $a$.${\it TA}$($a$); $l$,${\it tg}$.$M$($l$,${\it tg}$) )$\rightarrow$($x$:Id$\rightarrow$$T$($x$))$\rightarrow$($x$:Id$\rightarrow$$T$($x$)))
\\[0ex]$\times$(\=$k$:Knd$\rightarrow$kindcase($k$; $a$.${\it TA}$($a$); $l$,${\it tg}$.$M$($l$,${\it tg}$) )$\rightarrow$($x$:Id$\rightarrow$$T$($x$))$\rightarrow$\+
\\[0ex](($l$:IdLnk$\times$$t$:Id$\times$$M$($l$,$t$)) List))
\-\-
\end{tabbing}